Library hirst_inverse

Require Import PointsETC.

Open Scope R_scope.

Section Triangle.

Context `{M:triangle_theory}.

Definition hirst_inverse P U :=
 match P,U with
  cTriple p q r, cTriple u v w ⇒
  cTriple (q×r×u^2 - v×w×p^2) (r×p×v^2 - w×u×q^2) (p×q×w^2 - u×v×r^2)
 end.

Lemma X1_hirst_inverse_of_X1_X44 :
 eq_points X_1 (hirst_inverse X_1 X_44).
Proof.
intros.
red;simpl; repeat split; field; repeat split;try assumption.
Qed.

End Triangle.